Nuprl Lemma : Agatha Murder Puzzle (JProver)Lori2 8,37

Agatha hates Charles & Agatha hates Agatha
& (p:Person. p is richer than Agatha  The Butler hates p)
& (p:Person. Agatha hates p  Charles hates p)
& (p:Person. Agatha hates p  The Butler hates p)
& (p:Person. p likes Agatha  p likes The Butler  p likes Charles)
& (pq:Person. p kills q  p is richer than q)
& (pq:Person. p kills q  p hates q)
 The Butler did not kill Agatha & Charles did not kill Agatha 
latex


ProofTree


Definitionsx likes y, x did not kill y, A, x kills y, x:AB(x), P  Q, x:AB(x), x hates y, P & Q, x:AB(x), x is richer than y, P  Q, left+right, False

origin